home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
The World of Computer Software
/
The World of Computer Software.iso
/
proxy11.zip
/
PROXY.DOC
< prev
next >
Wrap
Text File
|
1992-12-29
|
59KB
|
1,921 lines
PROXY USERS GUIDE
Version 1.1
EDL Software Design
23419 S. Mirabella Circle
Boca Raton, FL 33433
Copyright (c) 1991, 1992, 1993 by Burt Leavenworth
All Rights Reserved
COPYRIGHT NOTICE
Proxy is not a public domain program. It is Copyright (C) 1991, 1992,
1993 by Burt Leavenworth.
LICENSE
Non-registered users are granted a limited license to use Proxy
on a trial basis for the purpose of determining whether Proxy is
suitable for their needs. Use of Proxy, except for this limited
purpose, requires registration (see the file PROXY.REG). Any
non-registered use, other than the above, is strictly prohibited.
No user may modify Proxy in any way, including but not limited to
decompiling, disassembling or otherwise reverse engineering the
program. All users are granted a limited license to copy Proxy
only for the trial use of others subject to the above limitations
provided that the full Proxy documentation, including license,
warranty and registration information, must be copied. No fee,
charge or other compensation may be accepted or requested by
any licensee.
Operators of electronic bulletin board systems (BBSs) may post
Proxy for downloading by their users only as long as the above
conditions are met. Distributors of user supported software
(disk vendors) may also distribute copies of Proxy subject to
the above conditions.
WARRANTY INFORMATION
The author hereby disclaims all warranties relating to this
software, whether express or implied, including without
limitation any implied warranties of merchantability or fitness
for a particular purpose. The author will not be liable for any
special, incidental, consequential, indirect or similar damages
including any lost profits or lost savings, arising from the use
of, or inability to use, this software, even if the author has
been advised of the possibility of such damages.
TABLE OF CONTENTS
Introduction ............................................ 2
Page 2
Getting Started ......................................... 2
Using Commands .......................................... 3
Primitive Types ....................................... 4
Identifiers ........................................... 4
Operators ............................................. 4
Sets .................................................. 4
Maps .................................................. 6
Sequences ............................................. 8
Strings ............................................... 10
Structs ............................................... 10
Operator Precedence ................................... 11
Function Definition ................................... 11
Class Definition ...................................... 12
System Commands ....................................... 14
Using Statements ........................................ 18
Assignment Statement .................................. 18
Conditional Statement ................................. 18
While Statement ....................................... 18
For Statement ......................................... 18
Return Statements ..................................... 19
I/O Statements ........................................ 19
Function Call ......................................... 20
Block ................................................. 20
Comments .............................................. 20
Type Predicates ......................................... 20
Class Constructors ...................................... 21
Scheme Interface ........................................ 21
An Example .............................................. 22
Another Example ......................................... 23
Proxy Keywords .......................................... 26
References .............................................. 27
Index ................................................... 27
INTRODUCTION
Proxy is an interpreter for a rapid prototyping language with C
and C++ like syntax based on modelling software using data
structures such as sets, maps, sequences, and objects. There are
no pointers or arrays in Proxy (although maps can be thought of
as a high level generalized array), which avoids the temptation
to use these rather low level types. Proxy has been influenced
to a great extent by the "me too"[1], VDM [3], EPROL [4], and
SETL [5] languages. Proxy allows the developer to make incremental
changes to a design, and test them immediately. It therefore
follows Fred Brooks' injunction: "Plan to throw one away: you
will, anyhow" [2].
A software system can be represented as a "state" and a collection of
functions which operate on components of the state. The user may
develop these operations incrementally or define them in files which
are loaded prior to execution. It is also possible to manipulate
objects (defined by classes) which encapsulate local states; this
allows the user to define a software model as a hierarchy of submodels.
Page 3
GETTING STARTED
The following files are provided with the Proxy system:
PROXY.EXE QUICKSRT.PRX
PROXY.DAT BINTREE.PRX
PROXY.INI TOPSORT.PRX
PROXY.DOC PRIMES.PRX
PROXY.REG CROSS.PRX
PRNTDOC.EXE EMAIL.PRX
PRINTDOC.BAT DATAFLOW.TXT
FINANCE.PRX READ.ME
Copy the files into a subdirectory of your choice. To install Proxy,
move to that subdirectory, type
proxy install
and press <enter>.
The install process will end with the message:
loading-ended
To run Proxy, type
proxy
After the copyright notice, the following will be displayed
on your screen:
Continue? : (run) / (exit)
>
Type (run) and press <enter>. Make sure that run is enclosed by
parentheses. A prompt ? will be displayed. You may now type
expressions and function definitions. To print out the
documentation, type printdoc and press <enter>. To get help
at any prompt, type: help; and press <enter>. To exit the
interpreter from any prompt, type exit; and press <enter>. Whenever
the Continue? : (run) / (exit) prompt appears, you may exit the
interpreter by typing (exit) and pressing <enter>.
Note - If you change to a new memory mapping scheme, for example,
upgrading to DOS 5.0, it will be necessary to re-install Proxy.
USING COMMANDS
There are two types of commands: "desk calculator" type commands,
and system commands. There are four system commands: load (to load
a Proxy file), transcript (to store in a file a transcript of all
subsequent keystrokes), help (to obtain the syntax of different
commands, statements, and composite data structures), and exit (to
Page 4
return to the DOS prompt). "Desk calculator" commands are the expressions,
assignments, and definitions that can be typed at the Proxy prompt for
immediate evaluation and execution.
Commands are typed at the Proxy prompt. The simplest command is an
expression to be evaluated, i.e. 2+2;. Note that every command
must be terminated with a semi-colon. There are four (primitive)
types of expressions.
Primitive types
The primitive data types are integer, real, boolean, and string.
Real literals are written in decimal form, i.e. 3.14159; there
must be at least one digit before the decimal point. Boolean
literals are written true, false, and strings are written with
double quotes, i.e. "This is a string".
Slightly more complicated expressions involve identifiers (variables):
Identifiers
All identifiers must start with a letter. The rest of the identifier
can consist of letters, underscores or digits. Identifiers are not
case sensitive, i.e. aBcD is considered to be the same identifier as
abcd.
Operators
The standard arithmetic, relational and Boolean operators are supported
wuth their relative precedence given by the following table:
! unary - highest
* / % && |
+ - || v
== != < > <= >= lowest
where ! represents logical negation, % is the modulo operator, && is
logical conjunction, || is logical disjunction, == represents equal
and != represents not equal.
Another command is assigning a value to an identifier. For example,
x=2;
We can then invoke the expression x+3;
More complicated expressions can be formed using the composite data
types provided by Proxy: sets, maps, sequences and structs.
Sets
A mathematical set is, of course, an unordered collection of elements.
From a formal point of view, each element should have the same type.
However, since Proxy has latent types, i.e. types are not declared by
Page 5
the programmer, set elements are not restricted to have the same type.
The simplest operation is to enumerate a set by delimiting its elements
by curly brackets:
{1,2,3,4,5}
This same set can be constructed by using the range notation
(not to be confused with the range of a map to be defined later)
{1..5}
Ranges can only be used when the elements are consecutive. Another
example of enumeration would be
smallprimes = {2,3,5,7};
To find the number of elements in the set smallprimes, we use the
cardinality operator card:
card smallprimes; returns 4
Two sets can be tested for equality using the equality operator ==.
Another simple operation is membership:
3 in smallprimes; returns true
3 notin smallprimes: returns false
To illustrate the standard operations of union, intersection, difference
subset and equality, we assume two sets s1 and s2 to have the values
s1={1,2,4,6};
s2={1,2,3,4,5};
s1 U s2; returns {1,2,3,4,5,6}
s1 inter s2; returns {1,2,4}
s1 diff s2; returns {6}
s1 subset s2; returns false
s1 == s2; returns false
The distributed union is the union of a set of sets. For example,
union {s1,s2,{6,7,8}}; returns {1,2,3,4,5,6,7,8}
The 'the' operator returns the only element of a singleton set. If
the argument is not a singleton set, an error message is returned.
the {13}; returns 13
The oneof operator applied to a set returns an 'arbitrary' element
of the set. However, Proxy always returns the 'first' element.
Page 6
oneof smallprimes; returns 2
The existential quantifier applied to a set and a predicate returns
true if there is at least one element of the set that satisfies the
predicate, and false otherwise. The universal quantitifer applied
to a set and a predicate returns true only if all elements of the set
satify the predicate.
(exists x in {2,3,5,7};even(x)); returns true
(all x in {2,3,5,7};even(x)); returns false
where the function even(x) returns true if x is even. The existential
quantifier above returns true because 2 satisfies even(2) and the
universal quantifier returns false because only even(2) is satisfied.
A more general way of constructing sets is given by the form:
{ f(x): x<- expr ; pred(x) }
where the syntax x<- expr is called a generator, and the syntax
; pred(x) is optional. The expression expr is evaluated to
yield a set. The values of the set are successively assigned to x
and a new set is formed from elements obtained by applying the function
f to the successive values of x which satisfy pred(x) (if pred(x) occurs).
Several examples will make this clearer.
{ x: x<- {1,2,3,4,5}}; returns {1,2,3,4,5}
This is the simplest case where f(x) is just x and a predicate does
not appear.
{ x: x <- {1,2,3,4,5};x>2}; returns {3,4,5}
{ x*x: x <- {1,2,3,4,5}}; returns {1,4,9,16,25}
It is possible to have two generators in which case an example is:
{ x+y: x <- {1,2}, y <- {3,4}} returns {4,5,6}
Only three elements are returned because two additions (1+4) and (2+3)
yield duplicate values.
Maps
Maps are also enumerated by delimiting their elements with curly
brackets (because formally maps are sets of ordered pairs). The
syntax is given by the following example.
m = {1->2,3->4,5->6};
where the first and second elements of each ordered pair is separated
Page 7
by the mapping symbol ->.
Maps can be constructed using map construction. In the following
example, len returns the length of a string.
{x->len x:x <- {"abc","defg","hijkl"}};
returns {"abc"->3,"defg"->4,"hijkl"->5}
The domain (range) of a map is obtained by forming a set composed
of all the first (second) elements of the ordered pairs
dom m; returns {1,3,5}
rng m; returns {2,4,6}
A single-valued map must have all its first elements unique. Notice
that, in general, card (rng m) <= card (dom m). The cardinality of
the range would be less, for example if
m = {1->2,3->2,5->6};
In this case, card(dom m) = 3, and card(rng m) = 2 (because of the
duplicate elements in the range).
Given a domain element, we can obtain the corresponding range element
using application (this is like a table lookup).
m[1]; returns 2
m[5]; returns 6
If a domain element is given which does not exist in the map, a false
value will be returned. However, it is possible to supply your own
value to be returned in this situation. This is done by supplying an
additional argument (called the default error return). For example,
m[7]; returns false
m[7,"not found"]; returns "not found"
Given a set of domain elements as a second argument, the image operation
(im) produces a set of the corresponding range elements (again assuming
m={1->2,3->4,5->6})
m im {3,5}; returns {4,6}
Domain restriction (dr) and domain subtraction (ds) produce new maps
from a given map by either allowing only certain domain elements in
the given map to appear in the result map, or taking away certain
domain elements from the given map. The domain elements are given
in a set which is the second argument of these operations.
{1->2,3->2,5->6} dr {3,5}; returns {3->2,5->6}
{1->2,3->2,5->6} ds {3,5}; returns {1->2}
The inverse operation just interchanges the domain and range elements
Page 8
of a map.
inverse {1->2,3->2,5->6}; returns {2->1,2->3,6->5}
Note that the result of the above operation is a multi-valued map.
The overwrite operation m1 overwr m2 is defined as follows: Each
mapping in m1 is included in the result, unless its domain element
occurs in the domain of m2. In that case, it is replaced by the
mapping from m2. Every mapping in m2 whose domain element does not
occur in the domain of m1 is included in the result. Example:
{1->2,3->4} overwr {3->5,4->6}; returns {1->2,3->5,4->6}
The map update m[d]=r is an assignment and a special case of
overwrite where the second operand (of overwrite) contains a
single ordered pair. Assuming that m is equal to {1->2,3->4},
m[3]=5; is equivalent to m overwr {3->5} and assigns to m the map
{1->2,3->5}.
Sequences
A sequence is a collection of ordered elements which may be
selected by their ordinal position (index) in the sequence. The
types of the elements are not necessarily the same.
A sequence can be enumerated by delimiting its elements by square
brackets:
[1,2,3,4,5]
This same sequence can be constructed by using the range (not to be
confused with the range of a map) notation:
[1..5]
Ranges can only be used when the elements are consecutive. Another
example of enumeration would be
s1 = [1,2,2,3,4];
Note the duplicate elements. To find the number of elements in the
sequence s1, we use the length operator len:
len s1; returns 5
Two sequences can be tested for equality using the equality operator
==. Concatenation of two sequences is performed used the concatenation
operator conc.
[1,2,3,4] conc [3,4,5]; returns [1,2,3,4,3,4,5]
If s=[3,4,5], then an element of the sequence can be selected using
its index in the sequence. For example,
Page 9
s[1]; returns 3
s[3]; returns 5
s[4]; returns false
s[4,0]; returns 0
The last example uses the default error return.
Other selection operators on sequences are hd, tl, last and butlast.
Hd returns the first element of the sequence. Tl returns a sequence
consisting of every element but the first. Last returns a sequence
consisiting of only the last element. Butlast returns a sequence
consisting of every element but the last.
hd s; returns 3
tl s; returns [4,5]
last s; returns [5]
butlast s; returns [3,4]
A sequence of length n can be represented by a map whose range elements
are the elements of the sequence, and whose domain elements are the
integers from 1 to n. Consequently, the domain operator applied to a
sequence will return the index elements {1..n}, and the range operator
will return the elements of the sequence contained in a set.
dom s; returns {1,2,3}
rng s; returns {3,4,5}
A sequence can be converted explicitly to its corresponding map and
conversely. Thus
m=seq2map s; assigns to m the map {1->3,2->4,3->5}
map2seq m; returns [3,4,5]
A more general way of constructing sequences, analogous to set
construction is given by the following form
[ f(x): x<- expr ; pred(x) ]
where the syntax x<- expr is called a generator, and the syntax
; pred(x) is optional. The expression expr is evaluated to
yield a sequence. The values of the sequence are successively assigned
to x and a new sequence is formed from elements obtained by applying the
function f to the successive values of x which satisfy pred(x) (if pred(x)
occurs). An example:
[len x: x<-["abc","defg","hijkl"];len x > 3]; returns [4,5]
Before concluding a discussion of sequences, it is important to point
out a distinction between a sequence of length two and an orderd pair.
Remember that a map may be considered to be a set of ordered pairs.
There are cases when one needs to access the components of an ordered
pair. Proxy provides two operators for this purpose, first and second.
Page 10
{first x:x<-{1->2,3->4,5->6}}; returns {1,3,5}
Suppose now that we have a set of sequences, say y={[1,2],[3,4]}
and we wish to obtain a set of the first elements of the sequences.
It would be wrong to write {first x:x<-y}. The correct solution is to
write {x[1]:x<-y}.
Strings
Strings can be considered to be sequences of characters, although
a character is not a primitive type in Proxy. Since the string
operators are similar to the sequence operators already discussed,
their use will be shown below in examples.
len "abcd"; returns 4
"abc" == "abc"; returns true
"abc" == "aBc"; returns false
"abc" < "abcd"; returns true
"abc" conc "defg"; returns "abcdefg"
s="abc";
s[2]; returns "b"
s[4]; returns false
s[4,0]; returns 0
hd "abc"; "a"
tl "abc"; "bc"
last "abc"; "c"
butlast "abc"; "ab"
Structs
Structs are data structures whose components may be selected by name.
The typical operations are declaration, instantiation, selection and
update.
A struct declaration is essentially a class declaration which defines
the names of the components of the struct. The syntax of the declaration
is best shown by an example.
struct item {partno, code, quantity;};
The above declaration defines item to be a struct with the (field)
names partno, code and quantity. Various items can be instantiated
(created) by providing the struct name and values for the fields.
(but a struct component may not be a function).
i1=new item(124,"receipt",15);
i2=new item(126,"issue",7);
Components of structs may be selected using a dot notation similar
to records in Pascal and structures in C.
i1.code; returns "receipt"
i2.quantity; returns 7
Page 11
Component values may be updated using assignment and dot notation.
i1.quantity=22; assigns 22 as the new value of the quantity
field.
Operator Precedence
The precedence of Proxy operators from highest to lowest are
shown below.
unary operators HIGHEST
* / % && inter conc dr ds im |
+ - || U overwr v
== != < > <= >= in notin subset equiv implies LOWEST
where the unary operators are:
- + ! hd tl last butlast card len first dom rng
union the oneof map2seq seq2map new inverse
Function Definition
The syntax of function definition in Proxy is the same as that in C
with minor differences: (1) the declaration of local variables is different
mainly due to the fact that the types of variables are not declared in
Proxy and (2) each function declaration in Proxy is terminated with a
semi-colon, (3) it is not necessary to name the top level function 'main',
(4) procedures do not require the prefix 'void'; in what follows we will
use the generic term function to apply as well to procedures. The syntax
is now shown:
identifier ( op-param-list op-decl) block ;
The definition consists of the function name (identifier) followed by
an optional parameter-list and an optional list of local variables
delimited by parentheses. The parameter-list consists of identifiers
separated by commas. The list of local variables consists of a semi-
colon followed by identifiers separated by commas. The block consists
of a statement-list (see the section on statements) delimited by
curly brackets. Finally, the definition must be terminated with a
semi-colon. Examples follow (the return statement is described in the
section on statements).
even(n) {return n%2==0;};
odd(n) {return !even(n);};
Given a subset of the integers, say digits={0..9};, we can define
a function to obtain the odd integers from this set.
odddigits() {return {n:n<-digits;odd(n)};};
The following example illustrates a simple recursive function to
add up the elements in an integer sequence.
Page 12
reduce(s) { if(s==[]) return 0; else return hd s + reduce(tl s);};
The next example illustrates the definition of a doubly recursive
function, and the declaration of a local variable x.
quicksort(s;x) { if(len s<2) return s;
x=s[1];
return quicksort([y:y<-s;y<x]) conc [x]
conc quicksort([y:y<-tl s;y>=x]);};
An example showing the use of the existential quantifier:
primes(max) {return [n:n<-[2..max];
!(exists m in {2..n-1};(n % m)==0)];};
An example of a procedure (a function which does not contain a return
statement) which has no parameters.
init() {x["a"]="b";};
This procedure initializes the variable x to the map {"a"->"b"}. The
same effect could have been achieved at the command level by the
assignment x["a"]="b";.
Class Definition and Instantiation
A class is defined by giving the class name, followed by an
enumeration of instance variables in the form of a
parameter list, followed by a collection of function definitions
(also called methods). Classes, contrary to C++, may only contain
functions.
In order to motivate the definition and usage of a class, let us first
define a simple queue. It does not matter what type of item the queue
contains; we will assume a queue of integers. In the specification
below, the state component q (a global variable) represents the queue
as a sequence, which is initialized as the empty sequence.
q=[];
enqueue(x) {q=q conc [x];};
dequeue(;x) {x=hd q;q=tl q;return x;};
empty() {return q==[];};
length() {return len q;};
A typical sequence of operations is:
? enqueue(3);
? enqueue(5);
? length();
2
Page 13
? dequeue();
3
? empty();
false
? dequeue();
5
? empty();
true
There are drawbacks to this approach. Only one queue is available, and
its representation is completely exposed. The problem can be solved by
defining a queue class.
class queue(rep) {
enqueue(x) {rep=rep conc [x];}
dequeue(;y) {y=hd rep;rep=tl rep; return y;}
empty() {return rep==[];}
length() {return len rep;}};
The coding is very similar except now the state component (rep) is local
and is hidden inside the class definition. The representation is
initialized from the outside and may only be changed indirectly by
invoking either the enqueue or dequeue operation. The analogous sequence
of operations is:
? q=new queue([]);
? q.enqueue(3);
? q.enqueue(5);
? q.length; or q.length();
2
? q.dequeue; or q.dequeue();
3
? q.empty; or q.empty();
false
? q.dequeue; or q.dequeue();
5
? q.empty; or q.empty();
true
? q;
object this shows the printed representation of an object
A second queue may be instantiated by using the new operation again.
Page 14
p=new queue([]);
and an arbitrary number of queues may be created in this way.
The function definitions may optionally be preceded by the keyword
public: to indicate that they are exported or made visible outside
the class. If the keyword public: is not used, the default is public.
There are cases when one wants to define functions that are private.
In this situation, the keywords private: and public: are used
(in that order). An example of a priority queue follows.
class pqueue(rep) {
private: insrt(x,y) {if(y == []) {rep = [x]; return rep;} else
if(x < hd y) {rep = [x] conc y;return rep;} else
{rep = [hd y] conc insrt(x,tl y);
return rep;}}
public: insert(x) {rep = insrt(x,rep); return rep;}
remove(;x) { if(rep == []) return "queue empty";
x = hd rep; rep = tl rep; return x;} };
The private declaration must be given first, followed by the public
declaration. The last statement in the insert function returns the
value of rep so that the user can see that the items are inserted in
sorted order.Alternatively, the string "ok" could be returned.
Note the declaration of the local variable x in the header of the
remove function. The following sequence of operations show calls to
the insert and remove functions:
? q= new pqueue([]);
? q.insert(3);
[3]
? q.insert(2);
[2,3]
? q.insert(9);
[2,3,9]
? q.insert(7);
[2,3,7,9]
? q.remove;
2
? q.remove;
3
? q.remove;
7
? q.remove;
9
? q.remove;
queue empty
Page 15
System Commands
The help command produces the following menu:
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 structs 8 quit
A "quick reference" screen showing functionality and syntax of Proxy
constructs is obtained by selecting one of the above numbers. The results
of selecting individual numbers is shown below.
1
COMMANDS
Type of Command Example
(1) an expression x + 3 ;
(2) function definition fun(y) {return y+1;};
(3) assignment y = 17;
(4) function call fun(3);
(5) struct declaration struct empl {age,citizen;};
(6) struct instantiation p = new empl(25, true);
(7) struct component update p.age = 26;
(8) map update table[3]= 4;
(9) class definition class stack(rep) {
push(x) {rep = [x] conc rep}
top() {return hd rep;}
pop() {rep= tl rep;} };
(10) class instantiation s= new stack([]);
(11) load command load "topsort.prx";
(12) transcript command transcript "session.txt";
(13) help command help;
(14) exit command exit;
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
2
FUNCTION DEFINITION
iden ( op-param-list op-decl) function definition
block ; where op-param-list is an
optional parameter list,
op-decl is an optional list
of local variables with the
form ;iden-list and block
consists of one or more
statements enclosed by
braces
Example
fact(n) { if (n=0) return 1;
else return n*fact(n-1);};
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
3
Page 16
STATEMENTS
left-hand-value = expr ; simple assignment, map update,
or struct component update
if ( expr ) stat1 conditional statement - form1
if ( expr ) stat1 ; conditional statement - form2
else stat2
while ( expr ) stat while statement
for iden <- expr ; stat for statament
return ; return statement - form1
return expr; return statement - form2
iden ( expr-list ); function call
{ stat1 ; ... statn ; } block
open(iden,"r") ; open read statement
open(iden,"w") ; open write statement
close(iden) ; close statement
readln(v1,...,vn) ; readln statement
readln(iden,v1,...vn) ; readln file statement
writeln(v1,...,vn) ; writeln statement
writeln(iden,v1,...,vn) ; writeln file statement
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
4
SETS
{ e1, e2, ..., en} set enumeration
{ e1 .. ek} set of integers from e1 to ek
{} empty set
{ e : x <- s } set comprehension
{ e : x <- s ; b } set comprehension with boolean
{ e : x <- s1 , y <- s2 } s1, s2 are sets
{ e : x <- s1 , y <- s2 ; b } b is a boolean
e in s set membership
e notin s set nonmembership
s1 inter s2 set intersection
s1 U s2 set union
s1 diff s2 set difference
s1 subset s2 subset
union s distributed union
card s cardinality of a set
s1 == s2 set equality
the s element of singleton set
oneof s arbitrary member of set
(all x in s ; b ) universal quantifier
(exists x in s ; b ) existential quantifier
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
5
MAPS
{ d1 -> r1, ..., dn -> rn } map enumeration
{} empty map
{ x -> e1 : x <- e2 } map construction
{ x -> e1 : x <- e2 ; b } map construction with boolean
dom m domain of map m
Page 17
rng m range of map m
m dr s domain restriction (s is a set)
m ds s domain subtraction (s is a set)
inverse m inverse of m
m im s image of m (s is a set)
m[x] application
m[x,r] application with default error return
m1 overwr m2 overwrite
m[d]= r map update
first p first element of ordered pair
second p second element of ordered pair
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
6
SEQUENCES
[ e1, e2, ..., en] sequence enumeration
[ e1 .. ek ] sequence of integers from e1 to ek
[] empty sequence
[ e : x <- s ] sequence construction
[ e : x <- s ; b ] sequence construction with boolean
[ e : x <- s1 , y <- s2 ] s1, s2 are sequences
[ e : x <- s1 , y <- s2 ; b ] b is a boolean
len s length of a sequence
s1 == s2 sequence equality
s1 conc s2 concatenation
s[i] selection
s[i,r] selection with default error return
hd s head of a sequence
tl s tail of a sequence
butlast s first n-1 elements
last s [s[len s]]
dom s set of indices of s
rng s set of elements of s
seq2map s convert sequence to a map
map2seq m convert map to a sequence
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
7
STRUCTS
struct sname { f1,...,fn; }; struct declaration
new sname(e1, ..., en) struct instantiation
s . fi ; struct component selection
s . fi = e ; struct component update
1 commands 2 fundef 3 statements 4 sets 5 maps 6 sequences 7 records 8 quit
The load command (an example of which is given above) is used to load
Proxy commands from a file. The commands are inserted in a file as
if they were being typed at the command line, the only difference being
that the last line in the file must contain the single token: end.
Be careful not to insert more than one command on a line. For example,
x=2; y=3; is wrong because only the first assignment would be executed.
A function or class definition, however, consists of only a single
command, although it can take up more than one line.
Page 18
The transcript command (an example of which is given above) is used to
record in a file all subsequent interactions of user inputs (keystrokes)
and resulting Proxy outputs.
The exit command terminates execution of the Proxy interpreter and
returns to the DOS prompt.
USING STATEMENTS
A statement is either a simple statement or a block (see below),
which is a sequence of statements delimited by curly brackets.
Assignment Statement
identifier = expression ; expression is evaluated and the
resulting value is stored in
identifier. Examples are:
x = {2, 3, 5, 7} ; simple assignment
m["Joe"] = 30; map update
p.r = {1->2, 3->4}; struct update
Conditional Statement
The conditional or if-statement may take one of the following
forms:
if ( expr ) stat1 in both cases, expr is evaluated;
if it evaluates to true then stat1
if ( expr ) stat1 ; else stat2 is executed. If it evaluates to
false, in the first case nothing
happens; in the second case stat2
is executed. Examples are:
if (x < 2) y = 0;
if (n == 0 ) f = 1; else f = n * f;
While statement
while ( expr ) stat expr is evaluated; as long as its
value is true, stat is executed,
and expr is reevaluated; when its
value is false, the following
statement is executed. Example:
while (n <= 10) n=n+1;
For statement
for identifier <- expr ; stat expr is evaluated and identifier
is assigned the values of the
resulting set or sequence; stat
is executed for each of these
Page 19
assignments. Example:
for i <- {1..10}; writeln(i);
Return statement
The return statement may take one of the following forms:
return ; the enclosing function is terminated.
return expr ; expr is evaluated and the enclosing
function is terminated with the value
of expr as its returned value. Example
return n+1;
I/O statements:
open(string,"r"); Opens a file for reading given by
string, and returns a file handle.
h = open("data.txt","r");
open(string,"w") ; Opens a file for writing given by
string, and returns a file handle.
close(identifier) ; Closes the file whose handle is
given by identifier.
close(h);
writeln(v1,...,vn) ; The scalar values or scalar valued
variables vi (integer, real, string,
boolean) are printed on one line
separated by spaces.
writeln(123,r,"order");
writeln(identifier,v1,...,vn) ; The values v1,...vn are output to
the file whose handle is given by
identifier.
writeln(h,123,r,"order");
readln(v1,...,vn) ; The variables v1,...vn (which must be
global) are assigned the corresponding
values input at the keyboard.
readln(a,b,c);
readln(identifier,v1,...vn) ; The variables v1,...vn are assigned
the corresponding values in the file
Page 20
whose handle is given by identifier.
If there are no more values in the file
to read, the global variable eof has
the value true, otherwise it has the
value false.
fun() {readln(h,a,b,c);
while(!eof) {writeln(a,b,c);
readln(h,a,b,c);}
};
Function call
identifier ( expr-list ) ; Each expr in expr-list is evaluated
and the function represented by
identifier is called with the
resulting arguments. If the function
call is not contained in an expression
i.e. it appears in a statement
context, the resulting value is
discarded.
Block
A sequence of statements may be grouped together to form a block
by enclosing them within curly brackets:
{ stat1 ;
stat2 ;
...
statn ;
} Notice that there is no semi-colon
after the closing bracket. Example:
while (bal>0) {int=bal*r;am=pay-int;bal=bal-am;n=n+1;}
Comments
The delimiter // starts a comment that terminates at the end of the
line on which it occurs. It may be preceded by a statement (not an
expression), whitespace or may appear at the beginning of the line.
TYPE PREDICATES
The following predicates are supplied to test the type of a given value.
is_number is_map
is_boolean is_seq
is_string is_struct
is_set
Example:
Page 21
is_number 3.14159; returns true
CLASS CONSTRUCTORS
When a class constructor is defined by the user, by declaring a method
with the same name as the class, the corresponding class object will
be initialized automatically when it is instantiated. Taking the queue
example again:
class queue(;rep) {
queue() {rep=[];}
enqueue(x) {rep = rep conc [x];}
dequeue(;y) {y = hd rep; rep = tl rep; return y;{{;
An instantiation for this class would have the syntax
iden = new queue();
where iden represents the name of the instantiated object.
Note that rep is defined as a local variable of the class, and that
the first method, named queue, initializes rep to the empty sequence.
When an object is instantiated, i.e. q = new queue(), the rep of that
object will be initialized.
SCHEME INTERFACE
Proxy is implemented by translating expressions and function definitions
into Scheme which is then executed by a Scheme interpreter. This
implementation allows Proxy functions to call Scheme functions which
can then send back results to the Proxy program. Since the list is the
quintessential data structure in Scheme, and since sets, maps and
sequences in Proxy are implemented in terms of lists, we provide
transition functions to perform the conversions. In going from Proxy
to Scheme, we use
$set2lst, $seq2lst, $map2lst (set, seq, map to list)
and from Scheme to Proxy, we use
$mkset, $mkseq, $mkmap (list to set, seq, map)
The $ prefix tells the translator that the function is to be found
in the Scheme name space rather than in the Proxy name space. By the
same token, variables in the Scheme name space must also be prefixed
by a $.
Consider the following artificial example. We first define a Scheme
function called fun, which when applied to a list of lists, returns
a list of all the second elements. In other words,
(fun '((1 2) (3 4))) returns (2 4)
Page 22
Fun is defined at the Proxy prompt, i.e.
Continue? : (run) / (exit)
> (define (fun x) (map (lambda (x) (cadr x)) x))
(run)
? $mkseq ( $fun ( $map2lst ( {1 -> 2, 3 -> 4} ))); returns [2, 4]
First, $map2lst is applied to the map to produce the list of lists:
((1 2) (3 4)). Then the Scheme function fun is applied to this to
produce the list (2 4). Finally $mkseq is applied to this to produce
the Proxy sequence [2, 4].
AN EXAMPLE
A "financial history" supports the following transactions:
receive(amount,source) records that amount (an integer) was
received from source (a string)
spend(amount,reason) records that amount (an integer) was
spent for reason (a string)
totalrec(source) returns the total amount received from
source
totalspent(reason) returns the total amount spent for
reason
cashonhand records the cash on hand (an integer)
There are three global variables representing the state: cashonhand,
inc (a map from source to amount), and exp (a map from reason to
amount).
The Proxy program for this example is contained in the file FINANCE.PRX
and is shown here exactly as contained in the file. Since types are not
declared in Proxy, it is good practice to specify the types of the state
components are shown below.
// state components:
// cashonhand: integer
// inc: map(string,integer)
// exp: map(string,integer)
receive(amount,source) {cashonhand=cashonhand+amount;
inc[source]=inc[source,0]+amount;
return "ok";};
spend(amount,reason) {if(amount>cashonhand) return "Insufficient funds";
cashonhand=cashonhand-amount;
exp[reason]=exp[reason,0]+amount;
return "ok";};
totalrec(source) {return inc[source,0];};
totalspent(reason) {return exp[reason,0];};
Page 23
cashonhand=100;
end
The cashonhand is initialized to 100 and is incremented in the receive
function and decremented in the spend function. If the amount to be
spent is greater than the cashonhand, the spend function returns
"Insufficient funds". The map 'inc' consists of a set of ordered pairs
where the first element of a pair is the source of a receipt, and the
second element is the total amount received from this source. The map
'exp' contains the pairs where the first element is the reason for the
expense and the second element is the total amount spent. The default
error return, for example inc[source,0], handles the case where a
source appears for the first time and therefore does not occur as a
domain element in the map. The totalrec and totalspent functions use map
application to return the total amounts received and spent respectively.
Here again, the default error return will return 0 if the source or
reason does not appear in the map.
Another way of writing the program is to leave out the return "ok"
statements in the spend and receive functions. The effect of these
changes is that no output will be obtained when they are invoked,
except in the case of insufficient funds.
A possible sequence of operations follows.
? cashonhand;
100
? spend(50,"food");
"ok"
? receive(100,"bank");
"ok"
? cashonhand;
150
? spend(100,"food");
"ok"
? totalspent("food");
150
? spend(150,"rent");
"Insufficient funds"
ANOTHER EXAMPLE
An Electronic Mail System (Email) is to be designed to provide
communication between users of the system. The following operations
must be supported:
Signon(u,p) - By giving a valid user name and user-selected password,
a user should be permitted access to the system.
Signoff(u) - The user may remove himself from the system
Add(u,n,p) - The "super" user may supply a name and password in order
Page 24
to add a new user to the list of authorized users.
Drop(u,n) - The "super" user may delete a user name from the list
of authorized users.
Send(u,t,n) - By giving the text of a message and name of a receiver,
a user can place a message into a receiver's queue.
Read(u) - A user can issue a Read command to examine his/her queue.
The response should be the sender's name and text of the
first message (if any). Successive reads will return
additional messages (if any).
Delete(u) - After reading a message, the user may issue a Delete
command to delete the message just read.
Reset(u) - This causes the next Read command to begin at the head
of the queue.
Notice that the first parameter of each operation represents the
name of the user invoking the operation.
A Proxy program for this application is contained in the file EMAIL.PRX.
This solution illustrates the use of return messages to signal exceptions.
A queue class is first defined with the following operations: read,
write, reset and delete. This class has two instance variables: procd
and remdr, both sequences. procd represents the queue of mail messages
already processed, and remdr represents the queue of messages not
yet read. The queue class acts like a sequential file and can be
used in any application requiring a data structure with these character-
istics. The state components are:
up (map from user to password)
uq (map from user to mail-queue)
so (set of users who are signed on)
// state components
// up: map(string,string)
// uq: map(string,queue)
// so: set(string)
class queue(procd,remdr) {
read() {var x;
if(len remdr=0) return "empty queue";
x:=hd remdr;
remdr:=tl remdr;
procd:=procd conc [x];
return x;}
write(msg) {remdr:=remdr conc [msg];}
reset() {remdr:=procd conc remdr;
procd:=[];}
delete() {if(len procd=0) return "empty queue";
procd:=butlast procd;} };
Page 25
up:={"super" -> "super"}; // initialize super user with pw "super"
uq:={"super" -> new queue([],[])};// initialize mail-queue so super user
// can send mail to him
mail :: sender text; // mail is a struct with two fields:
// sender and text
add(u,n,pw) {if (u /= "super") return {"not authorized",u};
uq[n]:=new queue([],[]); // initializes mail-queue
up[n]:=pw; // initializes password
return "ok";};
drop(u,n) {if (u /= "super") return {"not authorized",u};
if (n notin dom up) return {"unknown user",n};
up:=up ds {n}; // remove user and password
uq:=uq ds {n}; // remove user and mail-queue
if(n in so) so:=so diff {n}; // if user signed on, sign
return "ok";}; // him off
signon(u,pw) {if (up[u,""] /= pw) return {"incorrect password",pw};
so:=so U {u}; // sign him on
return "ok";};
signoff(u) {if (u notin so) return {"not signed on",u};
so:=so diff {u}; // sign him off
return "ok";};
send(u,t,r) {var x; if (u notin so) return {"not signed on",u};
if (r notin dom up) return {"unknown user",r};
x:=uq[r];
x.write(mk_mail(u,t)); // create mail and send
return "ok";};
read(u) {var x;if (u notin so) return {"not signed on",u};
x:=uq[u];
return x.read;}; // read mail
reset(u) {var x;if (u notin so) return {"not signed on",u};
x:=uq[u];
x.reset; // reset mail-queue
return "ok";};
delete(u) {var x;if (u notin so) return {"not signed on",u};
x:=uq[u];
x.delete; // delete mail
return "ok";};
so:= {};
end
The following sequence of messages and responses shows the application
of the Email operations.
? add("super","joe",123);
"ok"
? add("super","mike",456);
"ok"
? signon("joe",123);
"ok"
? signon("mike",455);
"incorrect password"
? signon("mike",456;
"ok"
Page 26
? send("joe","hello","mike");
"ok"
? send("joe","there","mike");
"ok"
? send("joe","meet me","tom");
{"unknown user","tom"}
? read("mike");
< "joe", "hello" >
? read("mike");
< "joe", "there" >
? read("mike");
"empty queue"
? reset("mike");
"ok"
? read("mike");
< "joe", "hello">
? delete("mike");
"ok"
? read("mike");
< "joe", "there" >
? reset("mike");
"ok"
? read("mike");
< "joe", "there" >
? drop("joe","mike");
{"not authorized","joe"}
? signoff("joe");
"ok"
This example illustrates the "me too" paradigm [1] for producing
prototypes in three steps:
(1) model step - identify the entities and associated operations of
an application. In this case, we selected mail and
queue as entities, and read, write, reset and
delete as operations on the queue.
(2) specification step - implement the entities and operations in
terms of sets, maps, sequences, etc.
We represented queue by a class with instance
variables procd and remdr. Mail was represented
by a struct with fields sender and text.
(3) validation step - the operations are executed to determine if the
model and implementation are appropriate.
The above steps are iterated as necessary until a satisfactory version
is obtained.
PROXY KEY WORDS
all len
butlast map2seq
card new
Page 27
class notin
close oneof
conc open
dom overwr
dr private
ds public
else readln
eof return
equiv rng
exists second
false seq2map
first struct
for subset
hd the
if tl
im true
implies U
in union
inter while
inverse writeln
last
REFERENCES
[1] Alexander, H. and Jones, V., Software Design and Prototyping using
me too, Prentice-Hall, New York, 1990.
[2] Brooks, F.,The Mythical Man-Month. Addison-Wesley, Reading, MA, 1975.
[3] Jones, C.B., Systematic Software Development Using VDM, Prentice-Hall,
New York, 1986.
[4] Hekmatpour, S. and Ince, D., Software Prototyping, Formal Methods and
VDM, Addison-Wesley, Reading, MA, 1988.
[5] Schwartz, J.T. et al, Programming with Sets: An Introduction to SETL,
Springer-Verlag, New York, 1986.
INDEX
assignment statement 3,8,10,12,15,17,18
block 11,15,16,18,20
boolean type 4,16,17,19
butlast operator 9,10,11,17
cardinality operator 5,7,16
class definition 12,13,15,17
classes 2,12
close statement 16
commands 3,4,14,15,16,17
comments 20
concatenation operator 8,17
conditional statement 16,18
default error return 7,9,17,21
difference operator 5,16
Page 28
distributed union operator 5,16
domain operator 7,8,9,16,21
domain restriction operator 7,16
domain subtraction operator 7,16
existential quantifier 6,12,16
exit command 3,15,18
first operator 6,7,9,10,11,17
for statement 18
function call 15,16
function definition 3,11,12,14,15
generator 6,9
hd operator 9,10,11,12,13,14,15,17
help command 3,14,15
identifiers 4,11,18,19,20
image operator 7,17
instantiation, class 12,13,15
instantiation, struct 10,15,17
intersection operator 5,16
inverse operator 7,11,17
i/o statement 9
integer type 4,9,11,12,16,17,19,20
last operator 9,10,11,17
len operator 7,8,9,10,11,12,13,17
load command 3,15,17
local variables 11,12,14,15
logical conjunction 4
logical disjunction 4
logical negation 4
main 11
map application 7,17,21
map construction 6,16
map enumeration 16
map update 8,15,17,18
map2seq operator 9,11,17
maps 4,6,7,15,16,17,25
membership operator 5,16
modulo operator 4
oneof operator 5,11,16
open statement 16,19
operators 4,9,10,11
operator precedence 11
overwrite operator 8,17
primitive types 4
private 14
procedures 11,12
public 14
range operator 7,8,9,16
readln statement 16,19,20
real type 4,19
return statement 11,12,13,14,15,16,19
second operator 6,7,9,17
seq2map operator 9,11,17
sequence construction 17
sequence enumeration 17
Page 29
sequence selection 9,17
sequence range 8
sequences 4,8,9,10,15,16,17,25
set constructor 5,6
set enumeration 16
set range 5
sets 4,6,15,16,17,25
statements 15,16,17,18,19,20
strings 4,10
structs 4,10,15,17
system commands 3,14
the operator 5
tl operator 9,10,11,12,13,14,15,17
transcript command 3,15,17
unary operators 4,11
union operator 5,11,16
universal quantifier 6,16
void 11
while statement 16,18,20
writeln statement 16,19,20
Page 30
